x, y:Atom1. ((x =a1 y))  x  y  Atom1  

latex

Definitions	P & Q, t  T, P  Q, , P  Q, a  b  T , P  Q, x:A. B(x)
Lemmas	assert of eq atom1, not functionality wrt iff, nequal wf, eq atom wf1, assert wf, not wf, iff functionality wrt iff